…64)

#3 isolated commit. ONLY placeholder SPDX lines staged; repo's other
uncommitted WIP deliberately left untouched/unstaged. PLMP/PMLP +
doubled = scaffold artifacts (LICENCE-POLICY.adoc A5), NOT relicensing.
Diff-shape asserted (SPDX-only). Refs standards LICENCE-POLICY.adoc A5.

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…ormance; #5 by-design (#121)

## What

Closes the **implementation ⇄ spec coupling** obligations
(`proofs/STATUS.md` §"Implementation ⇄ spec coupling") — making "the
soundness lives in the compiler" literally true, by **differential
conformance against the Coq-extracted verified artifacts** (the honest,
reproducible alternative to an infeasible full Rust-in-Coq refinement
proof).

| # | Coupling | Status |
|---|----------|--------|
| 1 | Rust checker refines Coq `check` (R5) | ✅ conformance-checked |
| 2 | Rust evaluator refines Coq `step` | ✅ conformance-checked |
| 3 | Echo modality wired surface → verified checker | ✅
conformance-checked (verified-core surface) |
| 4 | Rust session runtime refines Coq `cstep` (binary) | ✅
conformance-checked |
| 5 | Concrete `me` surface | ✅ by-design — not a gap |

## Method

The verified Coq functions are extracted to OCaml (`Extract.v`,
`Separate Extraction`) and used as **independent oracles**; the Rust
ports in `crates/my-qtt` are the implementations under test. One harness
(`conformance/run.sh`) generates a random corpus and asserts
byte-identical results. Where the spec is a *relation* (`step`,
`cstep`), a functional mirror is first **proved sound + complete** vs
the relation, then conformance-tested:

- **`Eval.v`** — `step1` + `step1_sound`/`step1_complete` (vs `step`),
axiom-free, in CI.
- **`SessionEval.v`** — `cstep1` + `cstep1_sound`/`cstep1_complete` (vs
`cstep`), axiom-free, in CI.

**60,000 results across 5 seeds agree** (3000 cases × {check, one-step,
normal-form, session-step}); the normal-form pass cross-checks the Rust
substitution against Coq's extracted `subst`, and echo terms (#3) ride
in the corpus.

## Files

- Coq (new, CI-gated): `Eval.v`, `SessionEval.v`; `Extract.v`
(extraction-only, not in suite).
- Harness: `conformance/{oracle.ml,run.sh,README.adoc}`,
`crates/my-qtt/src/bin/conformance_gen.rs`.
- Rust verified-core: `crates/my-qtt/src/{lib.rs (evaluator),session.rs
(new),surface.rs (echo tests)}`.
- `proofs/STATUS.md`: rows #1–#5 + new `conformance-checked` vocabulary
+ two mechanised-cores rows.

## Scope / honesty (carried in STATUS.md)

Refinement-by-conformance against the *extracted verified algorithm*,
not a full Rust-in-Coq proof. The *main* `checker.rs` (Hindley) still
doesn't call the verified core by default; echo lacks
conventional-compiler *syntax*; the n-ary `nstep`/`gstep` runtimes are a
larger follow-on. These are explicitly labelled, not hidden.

Requires `coqc` 8.18, `ocamlfind`+`ocamlc`, `cargo` (all in the proof CI
image).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

https://claude.ai/code/session_01BwV2DWsjkBiNP3oscimMLV

---
_Generated by [Claude
Code](https://claude.ai/code/session_01BwV2DWsjkBiNP3oscimMLV)_

---------

Co-authored-by: Claude <noreply@anthropic.com>